Dieser Audiobeitrag wird von der Universität Erlangen-Nürnberg präsentiert.

Herzlich willkommen. Sie merken schon, ich gehe heute in Ergesschaft vor als sonst.

Heute machen wir mal, was ernsthaft ist. Wir haben bisher gesehen,

Definitionen von Logiken, von ihrer Syntax und Semantik und genauer zu sein.

Und wir haben gesehen, ein Algorithmus, der uns Erfüllbarkeit entscheidet, so er das

dann tatsächlich tut. Wir haben uns die trivialen Teile der Algorithmenanalyse

überlegt, nämlich dass der Algorithmus terminiert und dass er korrekt antwortet,

wenn er nein sagt. So, es fehlt noch der, der schwierige Teil ist jetzt auch übertrieben,

so hart ist es dann auch nicht, aber der jedenfalls im Vergleich zu den anderen

Teilen, schwierigere Teil, nämlich zu zeigen, dass der Resolutionsalgorithmus recht hat,

wenn er ja sagt, also erfüllbar und weil das nicht wirklich abendfüllend ist, holen wir noch

nach die verbleibende Analyse unseres Systems natürlichen Schließen. Das System natürlichen

Schließen, das haben wir ja einfach nur präsentiert und ein paar Beispielanwendungen gemacht,

wie führt man denn nun also Beweise in diesem System. Wir hatten vorher eine Semantik definiert

und einen Begriff von logischer Konsequenz und wir haben uns bisher noch überhaupt keine Gedanken

gemacht, in welchem Verhältnis die beiden Begriffe eigentlich zueinander stehen und wir werden im

zweiten Teil der heutigen Sitzung zeigen, dass der Begriff der Beweisbarkeit mit dem Begriff

der logischen Folgerbarkeit zusammenhängt, also übereinstimmt, dasselbe. Auch das hat wieder einen

trivialen Teil, nämlich alles was ich beweisen kann ist auch eine logische Folgerung, das beweist man

mal so eben aus dem Ärmel. Der umgekehrte Teil, der ist dann substanzieller. Das alles vermittelt so ein

bisschen eine Idee davon, was der Logiker so in seinem Leben so tut. Der sitzt natürlich nicht

da und führt auf Papier irgendwelche Fitch-Beweise und freut sich, wenn er eine Formel bewiesen hat

oder sowas, sondern der macht eben solche logische Meta-Theorie. Also der zeigt, dass also von außen

betrachtet gewissermaßen die Logik bestimmte Eigenschaften hat, zum Beispiel eben ein vollständiges

Schlusssystem besitzt. Also wir befinden uns jetzt erstmal noch im Kapitel über den

Resolutionsalgorithmus. Ich schreibe nicht nochmal den ganzen Algorithmus an, ich schreibe nochmal

die Regel an, die er immer verwendet. Nicht die Regel, haben Sie schon gesehen, eben diese

sogenannte Resolutionsregel, die besagt, wenn ich in einer als Menge von Klauseln gelesenen CNF zwei

Klauseln des folgenden Formats habe, wiederum Klauseln gelesen als Mengen von Literalen, Klausel 1,

hier die linke enthält ein positives Literal A und die Klausel rechts enthält das entsprechende

negative Literal, dann kann ich die beiden Klauseln zusammenschmeißen und diese beiden Vorkommen von

dem Brust A hier wegwerfen, das heißt ich kann die Klausel C vereinigt D zu meiner CNF dazu fügen,

ohne ihre Erfüllbarkeit zu verändern. So und der Algorithmus, der wendet jetzt iterativ diese

Regel an, macht dabei die CNF, die vorliegt, immer größer, ohne dabei ihre Erfüllbarkeit zu ändern.

Er guckt immer nach, findet er zwischendurch diese leere Klausel hier und sobald er die findet,

sagt er nein, dann ist die CNF nicht erfüllbar, dass das so stimmen muss, das haben wir uns

letztes mal auch schon fertig überlegt und das ist eben auch sehr leicht zu sehen und...

Ja die andere Abbruchbedingungen, die ist ein bisschen kompliziert dazu schreiben,

ich schreibe sie trotzdem noch mal hin, weil wir genau das natürlich gleich brauchen, weil das eben

der Fall ist, der uns jetzt interessiert. Also immer dann, wenn er den Zustand erreicht hat,

wo er die Regel nicht mehr anwenden kann, dann bricht er ab und sagt ja, also erfüllbar und was

heißt es, dass die Regel nicht mehr anwendbar ist, nun das heißt immer wenn ich Klauseln dieses

Formats wie in der Prämisse verlangt in meiner CNF finde, dann ist die Konklusion der Resolutionsregel,

die Resolvente C V E D auch schon entfieh, das heißt er kann an dieser Stelle die Regel nicht

mehr anwenden, weil eben der Algorithmus so gebaut ist, dass er die Regel nicht anwendet, wenn sie

nichts Neues bringt. So. Und wir wollen jetzt zeigen Vollständigkeit des Algorithmus, wie gesagt

Terminierung und Korrektheit haben wir letztes Mal schon gezeigt. Und diese Korrektheitsaussage,

ich weiß diese Vollständigkeitsaussage, die heißt schlicht und einfach wenn der Algorithmus ja sagt,

dann stimmt das, also dann ist die CNF, die er da zu fassen hat, wirklich erfüllbar.

So, machen wir hieraus mal eine klar quantifizierte Aussage, hier ist natürlich gemeint, das hier